\begin{tabbing}
$i$ $>>$ $a$
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=Trans($i$):$k$:Knd$\rightarrow$kindtype($i$;$k$)$\rightarrow$state@$i$$\rightarrow$state@$i$$>>$$a$\+
\\[0ex]$\vee$ Send($i$):$k$:Knd$\rightarrow$kindtype($i$;$k$)$\rightarrow$state@$i$$\rightarrow$(Msg List)$>>$$a$
\\[0ex]$\vee$ Choose($i$):$b$:Id$\rightarrow$state@$i$$\rightarrow$(kindtype($i$;locl($b$))+Unit)$>>$$a$
\-
\end{tabbing}